\relax 
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\citation{eiffel,Meyer92-DbC}
\citation{MafLogozzo10}
\citation{BarnettFahndrichLogozzo-SAC-2010}
\citation{BarnettFahndrichLogozzo-SAC-2010}
\@writefile{toc}{\contentsline {title}{\unhbox \voidb@x \hbox {\hbox to\z@ {\hss Pre}condition} Inference from Intermittent \unhbox \voidb@x \hbox {Assert\hbox to\z@ {ions\hss }}\unskip \ \ignorespaces and Application to Contracts on Collections}{1}{chapter.1}}
\@writefile{toc}{\authcount {3}}
\@writefile{toc}{\contentsline {author}{Patrick Cousot, Radhia Cousot, Francesco Logozzo}{1}{chapter.1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{section.1.1}}
\@writefile{thm}{\contentsline {example}{{Example}{1}{}}{1}{example.1}}
\newlabel{ex-array}{{1}{1}{Introduction\relax }{example.1}{}}
\newlabel{cref@ex-array}{{[example][1][]1}{1}}
\citation{Cousot81-1-MuchnickJones}
\citation{Cousot78-1-TheseEtat}
\citation{BarnettFahndrichLogozzo-SAC-2010}
\citation{Cousot78-1-TheseEtat}
\@writefile{thm}{\contentsline {example}{{Example}{2}{}}{2}{example.2}}
\newlabel{ex-array-remove-side-effects}{{2}{2}{Introduction\relax }{example.2}{}}
\newlabel{cref@ex-array-remove-side-effects}{{[example][2][]2}{2}}
\@writefile{thm}{\contentsline {example}{{Example}{3}{}}{2}{example.3}}
\newlabel{ex-array-precondition}{{3}{2}{Introduction\relax }{example.3}{}}
\newlabel{cref@ex-array-precondition}{{[example][3][]3}{2}}
\citation{Cousot02-TCS}
\@writefile{toc}{\contentsline {section}{\numberline {2}Program semantics}{3}{section.1.2}}
\newlabel{sec:ProgramSemantics}{{2}{3}{Program semantics\relax }{section.1.2}{}}
\newlabel{cref@sec:ProgramSemantics}{{[section][2][]2}{3}}
\@writefile{toc}{\contentsline {subsubsection}{Small-step operational semantics.}{3}{section*.2}}
\@writefile{toc}{\contentsline {subsubsection}{Traces.}{3}{section*.3}}
\newlabel{eq:vectau+-fixpoint}{{1}{3}{Traces}{section*.3}{}}
\newlabel{cref@eq:vectau+-fixpoint}{{[equation][2][]2}{3}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Specification semantics}{3}{section.1.3}}
\newlabel{sec:SpecificationSemantics}{{3}{3}{Specification semantics\relax }{section.1.3}{}}
\newlabel{cref@sec:SpecificationSemantics}{{[section][3][]3}{3}}
\citation{Cousot02-TCS}
\citation{Dijkstra75-1}
\citation{CalcagnoEtAl-POPL09}
\citation{Dijkstra75-1}
\@writefile{toc}{\contentsline {section}{\numberline {4}The contract precondition inference problem}{4}{section.1.4}}
\newlabel{sec:ContractPreconditionInferenceProblem}{{4}{4}{The contract precondition inference problem\relax }{section.1.4}{}}
\newlabel{cref@sec:ContractPreconditionInferenceProblem}{{[section][4][]4}{4}}
\@writefile{thm}{\contentsline {definition}{{Definition}{4}{}}{4}{definition.4}}
\newlabel{def:PreconditionInferenceProblem}{{4}{4}{The contract precondition inference problem\relax }{definition.4}{}}
\newlabel{cref@def:PreconditionInferenceProblem}{{[definition][4][]4}{4}}
\newlabel{eq:no-new-run}{{2}{4}{The contract precondition inference problem\relax }{definition.4}{}}
\newlabel{cref@eq:no-new-run}{{[equation][4][]4}{4}}
\newlabel{eq:no-good-run-eliminated}{{3}{4}{The contract precondition inference problem\relax }{definition.4}{}}
\newlabel{cref@eq:no-good-run-eliminated}{{[equation][4][]4}{4}}
\@writefile{thm}{\contentsline {lemma}{{Lemma}{5}{}}{4}{lemma.5}}
\newlabel{no-good-run-ever-eliminated}{{5}{4}{The contract precondition inference problem\relax }{lemma.5}{}}
\newlabel{cref@no-good-run-ever-eliminated}{{[lemma][5][]5}{4}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{6}{}}{4}{theorem.1.4.6}}
\newlabel{StrongestPreconditionErrorAvoidability}{{6}{4}{The contract precondition inference problem\relax }{theorem.1.4.6}{}}
\newlabel{cref@StrongestPreconditionErrorAvoidability}{{[theorem][6][1]6}{4}}
\newlabel{eq:def-P-A}{{4}{4}{The contract precondition inference problem\relax }{theorem.1.4.6}{}}
\newlabel{cref@eq:def-P-A}{{[equation][5][](5)}{4}}
\citation{CousotCousot79-1-POPL}
\citation{Park69-FxpInd}
\citation{Cousot02-TCS}
\citation{Dijkstra75-1}
\citation{BaierKatoen08-POMC}
\citation{BiereEtAl03-BMC}
\@writefile{toc}{\contentsline {section}{\numberline {5}Basic elements of abstract interpretation}{5}{section.1.5}}
\newlabel{sec:ElementsAbstractInterpretation}{{5}{5}{Basic elements of abstract interpretation\relax }{section.1.5}{}}
\newlabel{cref@sec:ElementsAbstractInterpretation}{{[section][5][]5}{5}}
\@writefile{toc}{\contentsline {subsubsection}{Galois connections.}{5}{section*.4}}
\@writefile{toc}{\contentsline {subsubsection}{Fixpoint abstraction.}{5}{section*.5}}
\@writefile{thm}{\contentsline {lemma}{{Lemma}{7}{}}{5}{lemma.7}}
\newlabel{fixpoint-abstraction}{{7}{5}{Fixpoint abstraction}{lemma.7}{}}
\newlabel{cref@fixpoint-abstraction}{{[lemma][7][]7}{5}}
\@writefile{thm}{\contentsline {corollary}{{Corollary}{8}{David Park {\cite [Sect.\ 2.3]{Park69-FxpInd}}}}{5}{corollary.8}}
\newlabel{Park-dual-fixpoint}{{8}{5}{Fixpoint abstraction}{corollary.8}{}}
\newlabel{cref@Park-dual-fixpoint}{{[corollary][8][]8}{5}}
\@writefile{thm}{\contentsline {corollary}{{Corollary}{9}{}}{5}{corollary.9}}
\newlabel{dual-fixpoint-abstraction}{{9}{5}{Fixpoint abstraction}{corollary.9}{}}
\newlabel{cref@dual-fixpoint-abstraction}{{[corollary][9][]9}{5}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Fixpoint strongest contract precondition}{5}{section.1.6}}
\newlabel{sec:FixpointStrongestContractPrecondition}{{6}{5}{Fixpoint strongest contract precondition\relax }{section.1.6}{}}
\newlabel{cref@sec:FixpointStrongestContractPrecondition}{{[section][6][]6}{5}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{10}{}}{5}{theorem.1.6.10}}
\newlabel{fixpoint-P_A}{{10}{5}{Fixpoint strongest contract precondition\relax }{theorem.1.6.10}{}}
\newlabel{cref@fixpoint-P_A}{{[theorem][10][1]10}{5}}
\citation{Hecht-DFA77}
\citation{BarnettEtAl-IWACO07}
\@writefile{toc}{\contentsline {section}{\numberline {7}Contract precondition inference by symbolic flow analysis}{6}{section.1.7}}
\newlabel{sec:DataflowAnalysisContractPrecondition}{{7}{6}{Contract precondition inference by symbolic flow analysis\relax }{section.1.7}{}}
\newlabel{cref@sec:DataflowAnalysisContractPrecondition}{{[section][7][]7}{6}}
\newlabel{not-modified}{{1}{6}{Contract precondition inference by symbolic flow analysis\relax }{Item.1}{}}
\newlabel{cref@not-modified}{{[item][1][]1}{6}}
\newlabel{always-checked}{{2}{6}{Contract precondition inference by symbolic flow analysis\relax }{Item.2}{}}
\newlabel{cref@always-checked}{{[item][2][]2}{6}}
\@writefile{toc}{\contentsline {subsubsection}{Backward expression propagation.}{6}{section*.6}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{11}{}}{7}{theorem.1.7.11}}
\newlabel{soundness-dataflow-analysis}{{11}{7}{Backward expression propagation}{theorem.1.7.11}{}}
\newlabel{cref@soundness-dataflow-analysis}{{[theorem][11][1]11}{7}}
\@writefile{toc}{\contentsline {subsubsection}{Precondition generation.}{7}{section*.7}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{12}{}}{7}{theorem.1.7.12}}
\newlabel{soundness-data-flow-analysis}{{12}{7}{Precondition generation}{theorem.1.7.12}{}}
\newlabel{cref@soundness-data-flow-analysis}{{[theorem][12][1]12}{7}}
\@writefile{thm}{\contentsline {example}{{Example}{13}{}}{7}{example.13}}
\newlabel{modifications-are-not-taken-into-account}{{1}{7}{Precondition generation}{Item.3}{}}
\newlabel{cref@modifications-are-not-taken-into-account}{{[item][1][]1}{7}}
\newlabel{paths-are-not-taken-into-account}{{2}{7}{Precondition generation}{Item.4}{}}
\newlabel{cref@paths-are-not-taken-into-account}{{[item][2][]2}{7}}
\@writefile{toc}{\contentsline {section}{\numberline {8}Contract precondition inference for scalar variables by forward symbolic analysis}{7}{section.1.8}}
\newlabel{sec:ForwardSymbolicAnalysisContractPrecondition}{{8}{7}{Contract precondition inference for scalar variables by forward symbolic analysis\relax }{section.1.8}{}}
\newlabel{cref@sec:ForwardSymbolicAnalysisContractPrecondition}{{[section][8][]8}{7}}
\citation{Cousot78-1-TheseEtat}
\citation{King-CACM76}
\citation{Cousot78-1-TheseEtat}
\citation{CousotCousot77-3}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{14}{}}{8}{theorem.1.8.14}}
\@writefile{thm}{\contentsline {example}{{Example}{15}{}}{8}{example.15}}
\@writefile{toc}{\contentsline {section}{\numberline {9}Contract precondition inference by backward symbolic analysis}{9}{section.1.9}}
\newlabel{sec:BackwardSymbolicAnalysisContractPrecondition}{{9}{9}{Contract precondition inference by backward symbolic analysis\relax }{section.1.9}{}}
\newlabel{cref@sec:BackwardSymbolicAnalysisContractPrecondition}{{[section][9][]9}{9}}
\@writefile{toc}{\contentsline {subsubsection}{Backward symbolic precondition analysis of simple assertions.}{9}{section*.8}}
\@writefile{toc}{\contentsline {subsubsection}{Abstract domain.}{9}{section*.9}}
\@writefile{thm}{\contentsline {example}{{Example}{16}{}}{9}{example.16}}
\@writefile{toc}{\contentsline {subsubsection}{Backward path condition and checked expression propagation.}{10}{section*.10}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{17}{}}{10}{theorem.1.9.17}}
\newlabel{soundness-backward-analysis}{{17}{10}{Backward path condition and checked expression propagation}{theorem.1.9.17}{}}
\newlabel{cref@soundness-backward-analysis}{{[theorem][17][1]17}{10}}
\@writefile{thm}{\contentsline {example}{{Example}{18}{}}{10}{example.18}}
\newlabel{decrement-assert-positive}{{18}{10}{Backward path condition and checked expression propagation}{example.18}{}}
\newlabel{cref@decrement-assert-positive}{{[example][18][]18}{10}}
\@writefile{thm}{\contentsline {example}{{Example}{19}{}}{10}{example.19}}
\newlabel{assert-A-not-null}{{19}{10}{Backward path condition and checked expression propagation}{example.19}{}}
\newlabel{cref@assert-A-not-null}{{[example][19][]19}{10}}
\citation{CousotCousotLogozzo-09}
\@writefile{toc}{\contentsline {subsubsection}{Precondition generation.}{11}{section*.11}}
\@writefile{thm}{\contentsline {example}{{Example}{20}{}}{11}{example.20}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{21}{}}{11}{theorem.1.9.21}}
\@writefile{toc}{\contentsline {section}{\numberline {10}Contract precondition inference for collections by forward static analysis}{11}{section.1.10}}
\newlabel{sec:CollectionAnalysisContractPrecondition}{{10}{11}{Contract precondition inference for collections by forward static analysis\relax }{section.1.10}{}}
\newlabel{cref@sec:CollectionAnalysisContractPrecondition}{{[section][10][]10}{11}}
\@writefile{toc}{\contentsline {subsubsection}{Abstract domain for scalar variables.}{11}{section*.12}}
\@writefile{toc}{\contentsline {subsubsection}{Segmentation abstract domain.}{11}{section*.13}}
\@writefile{toc}{\contentsline {subsubsection}{Segmentation modification and checking analyses.}{12}{section*.14}}
\@writefile{thm}{\contentsline {example}{{Example}{22}{}}{12}{example.22}}
\@writefile{toc}{\contentsline {subsubsection}{Abstract domain for collections.}{13}{section*.15}}
\@writefile{toc}{\contentsline {subsubsection}{Collection segmentation concretization.}{13}{section*.16}}
\@writefile{toc}{\contentsline {subsubsection}{Segmented modification analysis concretization.}{14}{section*.17}}
\@writefile{toc}{\contentsline {subsubsection}{Segmented checking analysis concretization.}{14}{section*.18}}
\citation{CousotCousotLogozzo-09}
\citation{Dijkstra75-1}
\citation{FlanaganEtAL02-PLDI}
\citation{CousotCousot79-1-POPL}
\citation{CousotCousot-CC02,ChandraFinkSridharan09-PLDI}
\citation{Cousot78-1-TheseEtat}
\citation{CousotCousot92-2-JLP}
\citation{Cousot81-1-MuchnickJones}
\citation{Bourdoncle93-2,Rival-SAS05}
\citation{CalcagnoEtAl-POPL09,CousotCousot77-3,GulwaniTiwari-ESOP07}
\citation{ArnoutMeyer03-HiddenContracts}
\citation{CalcagnoEtAl-POPL09}
\citation{Dijkstra75-1}
\citation{MoyY-VMCAI08,Lev-AmiSagivRepsGulwani07-pre}
\citation{Cousot81-1-MuchnickJones}
\bibstyle{splncs03}
\bibdata{biblio}
\@writefile{toc}{\contentsline {subsubsection}{Segmented modification and checking analysis concretization.}{15}{section*.19}}
\@writefile{toc}{\contentsline {subsubsection}{Precondition generation.}{15}{section*.20}}
\newlabel{eq:precondition}{{4}{15}{Precondition generation}{section*.20}{}}
\newlabel{cref@eq:precondition}{{[equation][11][](11)}{15}}
\@writefile{thm}{\contentsline {theorem}{{Theorem}{23}{}}{15}{theorem.1.10.23}}
\@writefile{toc}{\contentsline {section}{\numberline {11}Related work, future work, and conclusions}{15}{section.1.11}}
\newlabel{sec:RelatedWorkConclusion}{{11}{15}{Related work, future work, and conclusions\relax }{section.1.11}{}}
\newlabel{cref@sec:RelatedWorkConclusion}{{[section][11][]11}{15}}
\bibcite{ArnoutMeyer03-HiddenContracts}{1}
\bibcite{BaierKatoen08-POMC}{2}
\bibcite{BarnettEtAl-IWACO07}{3}
\bibcite{BarnettFahndrichLogozzo-SAC-2010}{4}
\bibcite{BiereEtAl03-BMC}{5}
\bibcite{Bourdoncle93-2}{6}
\bibcite{CalcagnoEtAl-POPL09}{7}
\bibcite{ChandraFinkSridharan09-PLDI}{8}
\bibcite{Cousot78-1-TheseEtat}{9}
\bibcite{Cousot81-1-MuchnickJones}{10}
\bibcite{Cousot02-TCS}{11}
\bibcite{CousotCousot77-3}{12}
\bibcite{CousotCousot79-1-POPL}{13}
\bibcite{CousotCousot92-2-JLP}{14}
\bibcite{CousotCousot-CC02}{15}
\bibcite{CousotCousotLogozzo-09}{16}
\bibcite{Dijkstra75-1}{17}
\bibcite{MafLogozzo10}{18}
\bibcite{FlanaganEtAL02-PLDI}{19}
\bibcite{GulwaniTiwari-ESOP07}{20}
\bibcite{Hecht-DFA77}{21}
\bibcite{King-CACM76}{22}
\bibcite{eiffel}{23}
\bibcite{Meyer92-DbC}{24}
\bibcite{MoyY-VMCAI08}{25}
\bibcite{Park69-FxpInd}{26}
\bibcite{Rival-SAS05}{27}
\bibcite{Lev-AmiSagivRepsGulwani07-pre}{28}
